nms:(MaName List). Rnone()|nms = Rnone()  Realizer 

latex

Definitions	t  T, MaName, x:A. B(x), P  Q
Lemmas	MaName wf, Id wf, LocKnd wf, l disjoint nil, Rnone wf, trivial-R-restrict